﻿namespace Coq.MonoDevelop

open Ast

open System
open System.IO
open System.Diagnostics

open Coq.MonoDevelop.Helpers


type internal ProcessMessage = 
                 //Statement, location             //returns  errstring, start/end, line of error  
    | Process of list<(string*Location)> //* AsyncReplyChannel<option<string * option<int*int> * int>>
                 //position of cursor   //reply string for that position
    | Retrieve of Lexing.Position * AsyncReplyChannel<option<Message>>
                //position of cursor     //string that should be in the proof window
    | Proof of Lexing.Position * AsyncReplyChannel<string>
               //identifier name //reply string from compiler
    | Check of string * AsyncReplyChannel<string>

type Agent<'T> = MailboxProcessor<'T>

type ErrorResultEventArgs(s, i1, i2, sline, eline) = 
    inherit EventArgs()

    member x.Message = s
    member x.StartPos = i1
    member x.EndPos = i2
    member x.StartLine = sline
    member x.EndLine = eline
    member x.ContainsError = not (s="" || s=null)


type CoqProcessAgent () = 
    //Single instance of the CoqProcessAgent
    static let instance = CoqProcessAgent()

    //Instance of a CoqSession
    let ses = CoqSession()

    //Event
    let event1 = new Event<EventArgs>()

    //List of replies
    let mutable retList = list.Empty

    //Are we updating errors?
    let mutable updatingErrors = false

    //this creates a list of reactions for each statement
    let rec sendState state (result:list<Message*Location>) = 
        match state with 
        | [] -> result
        | (s,l)::t -> let (ss:string) = s
                      if (ss.Trim() <> "") then 
                         //Debug.WriteLine("sending----" + ss)
                         let r = ses.SendCommand(s)
                         match r with 
                         | Message.Error(s,i) -> (r,l)::result
                         | _  -> sendState t ((r,l)::result)
                      else 
                         sendState t result
    
    //finds last proof reaction or finds end of proof (that means the proof output windows will be empty)
    let rec findLastProof p rl = 
        match rl with 
        | [] -> ""
        | ((h,(b,e))::t) -> 
                    if (Common.IsBefore p b) then 
                        findLastProof p t 
                    else 
                        match h with 
                        | Message.Proof(p) -> p
                        | Message.Output(o) -> if (o.Contains("Proof completed.")) then ""
                                               else findLastProof p t 
                        | _ -> "" 


    //Async agent
    let agent = Agent.Start(fun agent -> 
        let rec loop prevstate = async {
            let! msg = agent.Receive()
            match msg with 
            | Process (state (*, reply*))->
                //restart session
                if (state.Length > 0) then 
                    updatingErrors <- true
                    ses.Restart() |> ignore
                    retList <- []
                    retList <- sendState state []
                    updatingErrors <- false
                if (retList.Length > 0) then
                    //positions of erroc command
                    let (h,(ps,pe)) = retList.Head
                    let ld = ps.Line - pe.Line |> Math.Abs
                    match h with 
                    | Message.Error(s,i) -> 
                        match i with 
                        | Some (i1, i2) -> 
                                let di = i1 - i2 |> Math.Abs
                                if (ld = 0 || (ld = 1 && pe.Column = 0)) then
                                    event1.Trigger(new ErrorResultEventArgs(s,ps.Column + 1 + i1, ps.Column + 1 + i1 + di , ps.Line, ps.Line))
                                else
                                    event1.Trigger(new ErrorResultEventArgs(s,ps.Column + 1 + i1, pe.Column, ps.Line, pe.Line))
                        | None          -> event1.Trigger(new ErrorResultEventArgs(s,ps.Column, pe.Column, ps.Line, pe.Line))
                    | _ -> event1.Trigger(new EventArgs())
                return! loop state
            | Proof (p, reply) ->
                reply.Reply(findLastProof p retList)
                return! loop prevstate
            | Check (c, reply) ->
                let dot = if (c.EndsWith(".")) then "" else "."
                let m = ses.SendCommand("\nCheck " + c + dot)
                match m with 
                | Message.Output(r) -> reply.Reply(r)
                | _ -> reply.Reply(null)
                return! loop prevstate
            | Retrieve (p,reply) ->
                let mR = List.tryFind (fun (_,(b,e)) -> Common.IsBefore b p) retList 
                match mR with 
                | Some (s,l) -> reply.Reply(Some(s))
                | None -> reply.Reply(None)
                return! loop prevstate         
        }
        loop [] )
    
    //Type Members
    [<CLIEvent>]
    member x.NotifyParsingFinished = event1.Publish

    member x.ProcessMessage(ssl) = 
        Debug.WriteLine("Sending to process")
        agent.Post(Process(ssl))

//    //Type Members
//    member x.ProcessMessage2(ssl) = 
//        Debug.WriteLine("Sending to process")
//        agent.PostAndReply(fun replyChan ->
//            Process(ssl, replyChan)
//        )
//
//    member x.AsyncProcessMessage(ssl, ?timeout) = 
//        agent.PostAndAsyncReply((fun replyChan ->
//            Process(ssl, replyChan)
//            ), ?timeout=timeout
//        ) 

    member x.CheckMessage(c) = 
        agent.PostAndReply(fun replyChan ->
            Check(c, replyChan)
        )

    member x.RetrieveMessage(p) = 
        agent.PostAndReply(fun replyChan ->
            Retrieve(p, replyChan)
        )

    member x.ProofMessage(p) = 
        agent.PostAndReply(fun replyChan ->
            Proof(p, replyChan)
        )

    /// Are we currently in the process of updating errors?
    member x.UpdatingErrors = updatingErrors

    /// Single instance of the language service
    static member Service = instance
    

